[FEAT] - Adapt the formal spec to include Linear Leios - #2278

Add two header-level checks to CHAINHEAD, derived from the certificate
inclusion rules of CIP-164: a header may only set certifiedEB if the last
applied block announced an endorser block, and if at least
3*leiosHeaderPeriod + leiosVotingPeriod + leiosDiffusionPeriod has elapsed
since that block.

The certifying header does not repeat the hash of the endorser block it
certifies, so LastAppliedBlock gains an aeb field recording what the last
block announced.

The three Leios periods are protocol parameters on PParams, read through
getPParams as maxHeaderSize already is, and named after their counterparts
in the ledger specification. They are wall-clock durations rather than slot
counts: constants in slots could be changed neither by governance nor by a
change of slot length. Milliseconds accordingly joins Coin in
Ledger.Prelude.Base, matching where the ledger specification defines it.

Comparing a duration against two slots needs a way to place a slot in time,
so EpochStructure gains slotToTime. Expressing the check as

  slotToTime sℓ + certificationDelay ps ≤ slotToTime s

rather than converting the delay into a slot count keeps certificationDelay
in the units CIP-164 states it in, and leaves the rounding implicit in the
arithmetic instead of fixing a rounding policy the CIP does not specify. A
function rather than a slot-length constant, so that an instantiation with
era-varying slot lengths remains expressible.

Note that the announced endorser block size is deliberately left unchecked:
per CIP-164 an incorrect size invalidates neither the header nor the block,
and only costs the producer the votes of honest nodes.

Split the Chain Head types figure in two, as it no longer fits on a page,
and give LastAppliedBlock and ChainHeadState separate AgdaSuppressSpace
blocks: sharing one made Agda emit an alignment preamble anchored past the
column of the ChainHeadState declaration, which LaTeX rejects.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The ledger specification's Leios design note settles how the summed periods
become a slot bound (docs/leios/design-note.md, "Alignment with the consensus
specification", item 2): CIP-164 converts them with the genesis slotLength,
rounded up, and both specifications are to share one definition of the
conversion and agree on the boundary sℓ + certificationDelay ≤ s.

So SlotLengthᶜ, nonzero, joins GlobalConstants, and durationToSlots sits
beside Milliseconds in Ledger.Prelude.Base. It takes the slot length as an
argument rather than naming SlotLengthᶜ, because the note has the conversion
travelling with Milliseconds and the constant travelling with the epoch
structure when both move to the common library; naming the constant would
fuse the two units.

This replaces the slotToTime formulation, which compared wall-clock times
instead of converting. That agreed with this one at every boundary, but it
was a second shape for a quantity the two specifications are meant to share,
which is what the note exists to prevent.

EpochStructure keeps a field for the conversion, as Slot is abstract and only
the structure can present durationToSlots' result as one. The ledger
specification's Slot is abstract in the same way, so its certificationDelay
will need the same; if it lands a different shape, this should follow.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The dummy periods summed to 8000ms against a slot length of 1000ms, so the
delay was a whole number of slots and rounding down would have given the same
answer; the cases also certified at slots 2 and 10 against a delay of 8,
leaving the boundary untested.

leiosDiffusionPeriod becomes 3500ms, so the delay is ⌈8500/1000⌉ = 9 where
rounding down would give 8, and two cases pin the boundary: slot 8 is
rejected, slot 9 accepted. Replacing the ceiling with a floor now fails the
first of those and nothing else.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

slotsFromDuration was a field, so only ℕEpochStructure rounded up and any
other instance could shorten the delay, or ignore the duration entirely,
without the specification noticing. The rounding is what CIP-164's Step 5
specifies and what its security argument depends on.

EpochStructure now takes the genesis SlotLength as a constant and derives
slotsFromDuration from it, so the rounding holds by construction. ℕtoSlot
injects the resulting count into the slot semiring, as ℕtoEpoch already does
for epochs; this relies on 1# denoting one slot, which addSlot and firstSlot
assume too.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The header's certifiedEB bit obliging the body to carry a matching
certificate is enforced by the ledger, not here, so do not present it as a
header-only check.

The subsection enumerates what the chain head state consists of, and adding
the aeb field to LastAppliedBlock left that list describing a state one
component smaller than the figure beside it shows.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Co-authored-by: Sebastian Nagel <ch1bo@users.noreply.github.com>